Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixes to equiv_simple #3971

Merged
merged 3 commits into from
Dec 18, 2023
Merged

Fixes to equiv_simple #3971

merged 3 commits into from
Dec 18, 2023

Conversation

povik
Copy link
Member

@povik povik commented Oct 2, 2023

Fix how equiv_simple walks over signals back in time and extend the flip-flop support to all kinds of purely synchronous flip-flops.

@povik povik mentioned this pull request Oct 2, 2023
Open
@povik
Copy link
Member Author

povik commented Oct 2, 2023

Huh, got a failure on Jenkins.

http://51.15.92.24:8080/job/Yosys-PR/375/consoleFull

...
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Assert failed in top: sva_value_change_changed.sv:7.2-9.4 ($auto$verificsva.cc:1731:import$23)
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: ##   0:00:00  Status: failed
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: finished (returncode=1)
SBY  9:53:39 [sva_value_change_changed_pass] engine_0: Status returned by engine: FAIL
SBY  9:53:39 [sva_value_change_changed_pass] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  9:53:39 [sva_value_change_changed_pass] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  9:53:39 [sva_value_change_changed_pass] summary: engine_0 (smtbmc yices) returned FAIL
SBY  9:53:39 [sva_value_change_changed_pass] summary: counterexample trace: sva_value_change_changed_pass/engine_0/trace.vcd
SBY  9:53:39 [sva_value_change_changed_pass] summary:   failed assertion top.$auto$verificsva.cc:1731:import$23 at sva_value_change_changed.sv:7.2-9.4 in step 2
SBY  9:53:39 [sva_value_change_changed_pass] DONE (FAIL, rc=2)
make: *** [Makefile:7: sva_value_change_changed.ok] Error 2

@jix, any ideas on what the interaction of equiv_simple and SBY would be?

@povik
Copy link
Member Author

povik commented Oct 2, 2023

This appears to be an issue with the CI setup itself rather than the PR.

povik added 3 commits October 3, 2023 13:05
@povik
equiv_simple: Drop hollow conditional
26644ea 
All the listed flip-flop types would be known cells, so the extra part
of the conditional is without effect.
@povik
equiv_simple: Do not special-case flip-flop types in cone expansion
dbf11da 
If there's an asynchronous flip-flop type, it will be caught by not
having a synchronous SAT model later on. Otherwise we can support all
flip-flops.
@povik
equiv_simple: Fix seed handling in non-short mode
1f1f43e
@povik povik force-pushed the equiv_simple-fixes branch from 4278f16 to 1f1f43e Compare October 3, 2023 11:05
@nakengelhardt nakengelhardt merged commit 78541be into YosysHQ:master Dec 18, 2023
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@povik @ArkadyKlimov @nakengelhardt